w:World, a, b:E. FairFifo  (w_locl(w;a;b)  loc(a) = loc(b)  Id & a < b) 

latex

Definitions

t  T, x:A. B(x), FairFifo, x:AB(x), E, e < e', x:AB(x), P  Q, World, time(e), a<b, w-info(w;e), x.A(x), loc(e), Id, s = t, P & Q, w_locl(w;x;y), P  Q, , {x:A| B(x) }, Type, Prop, w-pred(w;e), pred(e), first(e), b, A, A & B, rel_exp(T;R;n), f(a), , x:A. B(x), P  Q, x f y, R^+, i=j, {T}, SQType(T), , s ~ t, #$n, left+right, P  Q, Dec(P), AB, Void, False, <a,b>, b, , Unit, n-m, -n, n+m, loc(e), a(i;t), isnull(a), Atom$n, ij, x. t(x), 2of(t), 1of(t)

Lemmas

w locl wf, cless wf, w-cless-loc, pi1 wf, pi2 wf, rel exp add, ge wf, nat properties, w-pred-bound, w-loc-lemma, Id sq, w-isnull wf, w-a wf, decidable lt, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, w-loc-w-pred, w-pred-decreases, nat plus properties, le wf, decidable int equal, nat plus wf, rel exp wf, nat plus inc, not wf, assert wf, first wf, pred wf, w-pred wf, loc wf, Id wf, w-info wf, w-time wf, nat wf, world wf, w-E wf, fair-fifo wf